Hoare Logic.md (2527B)
1 +++ 2 title = 'Hoare Logic' 3 +++ 4 # Hoare Logic 5 For reasoning about concrete programs. 6 7 ## Hoare triples 8 Have the form `{P} S {Q}`, where `S` is statement, `P` (precondition) and `Q` (postcondition) are logical formulas over state variables. 9 10 Meaning: if `P` holds before `S` is executed and execution terminates normally, `Q` holds at termination. 11 Is partial correctness statement, i.e. program is correct if it terminates normally. 12 13 Examples: 14 15 ``` 16 {true} b := 4 {b = 4} 17 {b ≥ 5} b := b + 1 {b ≥ 6} 18 ``` 19 20 ## Semantic approach to Hoare Logic 21 We can define Hoare triples semantically in Lean. 22 Use predicates on states (`state → Prop`) to represent pre and postconditions. 23 24 ```lean 25 def partial_hoare (P : state → Prop) (S : stmt) (Q : state → Prop) : Prop := 26 ∀s t, P s → (S, s) ⟹ t → Q t 27 28 notation `{* ` P : 1 ` *} ` S : 1 ` {* ` Q : 1 ` *}` := 29 partial_hoare P S Q 30 ``` 31 32 Using it for a program exchanging two variables (in WHILE): 33 34 ```lean 35 def SWAP : stmt := 36 stmt.assign "t" (λs, s "a") ;; 37 stmt.assign "a" (λs, s "b") ;; 38 stmt.assign "b" (λs, s "t") 39 40 lemma SWAP_correct (a₀ b₀ : Ν) : 41 {* λs, s "a" = a₀ ∧ s "b" = b₀ *} 42 SWAP 43 { * λs, s "a" = b₀ ∧ s "b" = a₀ *} := 44 begin 45 /- 46 proof of correctness 47 -/ 48 sorry 49 end 50 ``` 51 52 Program adding two numbers: 53 54 ```lean 55 def ADD : stmt := 56 stmt.while (λs, s "n" ≠ 0) 57 (stmt.assign "n" (λs, s "n" - 1) ;; 58 stmt.assign "m" (λs, s "m" + 1)) 59 60 lemma ADD_correct (n₀ m₀ : Ν) : 61 {* λs, s "n" = n₀ ∧ s "m" = m₀ *} 62 ADD 63 {* λs, s "n" = 0 ∧ s "m" = n₀ + m₀ *} := 64 begin 65 /- 66 proof here 67 -/ 68 sorry 69 ``` 70 71 ## Verification condition generator 72 Program that applies Hoare rules automatically and produce verification conditions, which have to be proved by user. 73 User must provide strong enough loop invariants as annotations. 74 75 An invariant must be true before loop, remain true for each iteration if true before loop, and be strong enough to imply desired loop postcondition. 76 Suitable invariants tend to be: work done + work remaining = desired result. 77 78 VCGs usually work backward from postcondition, using backward rules (rules sated to have some `Q` as postcondition). 79 80 ## Hoare triples for total correctness 81 Total correctness: program not only partially correct, but always terminates. 82 Of the form `[P] S [Q]`: if `P` holds before `S` runs, the execution terminates normally and `Q` holds in the final state. 83 Loops must then be annotated by a variant `V` (natural number that decreases with each iteration). 84